unsolvable M.pre(a,s) == P != (M.2.2.2).1(a)  ((P(s))) 

latex

---

clarification:

unsolvable M.pre(a,s) == fpf-val(IdDeq; ((M.2.2.2).1); a; a,P.(((P(s))))) 

latex

Definitions	z != f(x)  P(a;z), IdDeq, t.1, t.2, A, b, f(a)
FDL editor aliases	ma-npre